$\forall$${\it es}$:ES. SWellFounded(es{-}pred!(${\it es}$;$e$;${\it e'}$))